Termination w.r.t. Q proof of /tmp/tmpEhvz9w/ExIntrod_GM01

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

ACTIVE(nats) → ADX(zeros)
MARK(adx(X)) → ACTIVE(adx(mark(X)))
TAIL(active(X)) → TAIL(X)
MARK(head(X)) → MARK(X)
MARK(tail(X)) → MARK(X)
ACTIVE(incr(nil)) → MARK(nil)
MARK(cons(X1, X2)) → MARK(X1)
CONS(X1, mark(X2)) → CONS(X1, X2)
INCR(active(X)) → INCR(X)
HEAD(mark(X)) → HEAD(X)
ACTIVE(zeros) → CONS(0, zeros)
ACTIVE(incr(cons(X, L))) → INCR(L)
MARK(head(X)) → HEAD(mark(X))
MARK(tail(X)) → TAIL(mark(X))
INCR(mark(X)) → INCR(X)
S(active(X)) → S(X)
ADX(active(X)) → ADX(X)
MARK(cons(X1, X2)) → CONS(mark(X1), X2)
MARK(tail(X)) → ACTIVE(tail(mark(X)))
HEAD(active(X)) → HEAD(X)
TAIL(mark(X)) → TAIL(X)
ACTIVE(incr(cons(X, L))) → CONS(s(X), incr(L))
MARK(zeros) → ACTIVE(zeros)
ACTIVE(adx(cons(X, L))) → CONS(X, adx(L))
MARK(adx(X)) → ADX(mark(X))
CONS(active(X1), X2) → CONS(X1, X2)
ACTIVE(nats) → MARK(adx(zeros))
CONS(mark(X1), X2) → CONS(X1, X2)
MARK(s(X)) → MARK(X)
MARK(incr(X)) → INCR(mark(X))
MARK(incr(X)) → MARK(X)
MARK(incr(X)) → ACTIVE(incr(mark(X)))
ACTIVE(adx(cons(X, L))) → MARK(incr(cons(X, adx(L))))
CONS(X1, active(X2)) → CONS(X1, X2)
ACTIVE(adx(cons(X, L))) → ADX(L)
MARK(s(X)) → ACTIVE(s(mark(X)))
ADX(mark(X)) → ADX(X)
ACTIVE(incr(cons(X, L))) → S(X)
MARK(s(X)) → S(mark(X))
ACTIVE(adx(cons(X, L))) → INCR(cons(X, adx(L)))
S(mark(X)) → S(X)
ACTIVE(incr(cons(X, L))) → MARK(cons(s(X), incr(L)))
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(head(X)) → ACTIVE(head(mark(X)))
MARK(adx(X)) → MARK(X)
ACTIVE(head(cons(X, L))) → MARK(X)
ACTIVE(adx(nil)) → MARK(nil)
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(0) → ACTIVE(0)
MARK(nats) → ACTIVE(nats)
MARK(nil) → ACTIVE(nil)
ACTIVE(tail(cons(X, L))) → MARK(L)

The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(nats) → ADX(zeros)
MARK(adx(X)) → ACTIVE(adx(mark(X)))
TAIL(active(X)) → TAIL(X)
MARK(head(X)) → MARK(X)
MARK(tail(X)) → MARK(X)
ACTIVE(incr(nil)) → MARK(nil)
MARK(cons(X1, X2)) → MARK(X1)
CONS(X1, mark(X2)) → CONS(X1, X2)
INCR(active(X)) → INCR(X)
HEAD(mark(X)) → HEAD(X)
ACTIVE(zeros) → CONS(0, zeros)
ACTIVE(incr(cons(X, L))) → INCR(L)
MARK(head(X)) → HEAD(mark(X))
MARK(tail(X)) → TAIL(mark(X))
INCR(mark(X)) → INCR(X)
S(active(X)) → S(X)
ADX(active(X)) → ADX(X)
MARK(cons(X1, X2)) → CONS(mark(X1), X2)
MARK(tail(X)) → ACTIVE(tail(mark(X)))
HEAD(active(X)) → HEAD(X)
TAIL(mark(X)) → TAIL(X)
ACTIVE(incr(cons(X, L))) → CONS(s(X), incr(L))
MARK(zeros) → ACTIVE(zeros)
ACTIVE(adx(cons(X, L))) → CONS(X, adx(L))
MARK(adx(X)) → ADX(mark(X))
CONS(active(X1), X2) → CONS(X1, X2)
ACTIVE(nats) → MARK(adx(zeros))
CONS(mark(X1), X2) → CONS(X1, X2)
MARK(s(X)) → MARK(X)
MARK(incr(X)) → INCR(mark(X))
MARK(incr(X)) → MARK(X)
MARK(incr(X)) → ACTIVE(incr(mark(X)))
ACTIVE(adx(cons(X, L))) → MARK(incr(cons(X, adx(L))))
CONS(X1, active(X2)) → CONS(X1, X2)
ACTIVE(adx(cons(X, L))) → ADX(L)
MARK(s(X)) → ACTIVE(s(mark(X)))
ADX(mark(X)) → ADX(X)
ACTIVE(incr(cons(X, L))) → S(X)
MARK(s(X)) → S(mark(X))
ACTIVE(adx(cons(X, L))) → INCR(cons(X, adx(L)))
S(mark(X)) → S(X)
ACTIVE(incr(cons(X, L))) → MARK(cons(s(X), incr(L)))
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(head(X)) → ACTIVE(head(mark(X)))
MARK(adx(X)) → MARK(X)
ACTIVE(head(cons(X, L))) → MARK(X)
ACTIVE(adx(nil)) → MARK(nil)
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(0) → ACTIVE(0)
MARK(nats) → ACTIVE(nats)
MARK(nil) → ACTIVE(nil)
ACTIVE(tail(cons(X, L))) → MARK(L)

The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 7 SCCs with 18 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

TAIL(active(X)) → TAIL(X)
TAIL(mark(X)) → TAIL(X)

The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

TAIL(active(X)) → TAIL(X)
TAIL(mark(X)) → TAIL(X)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(active(x₁)) = 9/4 + x_1
POL(mark(x₁)) = 1/2 + (3/2)x_1
POL(TAIL(x₁)) = (1/2)x_1

The value of delta used in the strict ordering is 1/4.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

HEAD(mark(X)) → HEAD(X)
HEAD(active(X)) → HEAD(X)

The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

HEAD(mark(X)) → HEAD(X)
HEAD(active(X)) → HEAD(X)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(active(x₁)) = 1/2 + (3/2)x_1
POL(mark(x₁)) = 9/4 + x_1
POL(HEAD(x₁)) = (1/2)x_1

The value of delta used in the strict ordering is 1/4.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ADX(active(X)) → ADX(X)
ADX(mark(X)) → ADX(X)

The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

ADX(active(X)) → ADX(X)
ADX(mark(X)) → ADX(X)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(active(x₁)) = 9/4 + x_1
POL(ADX(x₁)) = (1/2)x_1
POL(mark(x₁)) = 1/2 + (3/2)x_1

The value of delta used in the strict ordering is 1/4.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

S(mark(X)) → S(X)
S(active(X)) → S(X)

The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

S(mark(X)) → S(X)
S(active(X)) → S(X)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(active(x₁)) = 1/2 + (3/2)x_1
POL(mark(x₁)) = 9/4 + x_1
POL(S(x₁)) = (1/2)x_1

The value of delta used in the strict ordering is 1/4.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CONS(X1, active(X2)) → CONS(X1, X2)
CONS(mark(X1), X2) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, mark(X2)) → CONS(X1, X2)

The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

CONS(X1, active(X2)) → CONS(X1, X2)
CONS(X1, mark(X2)) → CONS(X1, X2)

The remaining pairs can at least be oriented weakly.

CONS(mark(X1), X2) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)

Used ordering: Polynomial interpretation [25,35]:

POL(active(x₁)) = 1/4 + (3/2)x_1
POL(CONS(x₁, x₂)) = (4)x_2
POL(mark(x₁)) = 4 + (4)x_1

The value of delta used in the strict ordering is 1.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CONS(mark(X1), X2) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)

The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

CONS(mark(X1), X2) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(active(x₁)) = 1/2 + (3/2)x_1
POL(CONS(x₁, x₂)) = (1/2)x_1
POL(mark(x₁)) = 9/4 + x_1

The value of delta used in the strict ordering is 1/4.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

INCR(mark(X)) → INCR(X)
INCR(active(X)) → INCR(X)

The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

INCR(mark(X)) → INCR(X)
INCR(active(X)) → INCR(X)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(active(x₁)) = 1/2 + (3/2)x_1
POL(mark(x₁)) = 9/4 + x_1
POL(INCR(x₁)) = (1/2)x_1

The value of delta used in the strict ordering is 1/4.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(nats) → MARK(adx(zeros))
MARK(adx(X)) → ACTIVE(adx(mark(X)))
ACTIVE(incr(cons(X, L))) → MARK(cons(s(X), incr(L)))
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(s(X)) → MARK(X)
MARK(tail(X)) → MARK(X)
MARK(head(X)) → MARK(X)
MARK(tail(X)) → ACTIVE(tail(mark(X)))
MARK(head(X)) → ACTIVE(head(mark(X)))
MARK(incr(X)) → ACTIVE(incr(mark(X)))
MARK(incr(X)) → MARK(X)
MARK(cons(X1, X2)) → MARK(X1)
ACTIVE(adx(cons(X, L))) → MARK(incr(cons(X, adx(L))))
MARK(adx(X)) → MARK(X)
MARK(zeros) → ACTIVE(zeros)
ACTIVE(head(cons(X, L))) → MARK(X)
MARK(s(X)) → ACTIVE(s(mark(X)))
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(nats) → ACTIVE(nats)
ACTIVE(tail(cons(X, L))) → MARK(L)

The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(s(X)) → ACTIVE(s(mark(X)))

The remaining pairs can at least be oriented weakly.

ACTIVE(nats) → MARK(adx(zeros))
MARK(adx(X)) → ACTIVE(adx(mark(X)))
ACTIVE(incr(cons(X, L))) → MARK(cons(s(X), incr(L)))
MARK(s(X)) → MARK(X)
MARK(tail(X)) → MARK(X)
MARK(head(X)) → MARK(X)
MARK(tail(X)) → ACTIVE(tail(mark(X)))
MARK(head(X)) → ACTIVE(head(mark(X)))
MARK(incr(X)) → ACTIVE(incr(mark(X)))
MARK(incr(X)) → MARK(X)
MARK(cons(X1, X2)) → MARK(X1)
ACTIVE(adx(cons(X, L))) → MARK(incr(cons(X, adx(L))))
MARK(adx(X)) → MARK(X)
MARK(zeros) → ACTIVE(zeros)
ACTIVE(head(cons(X, L))) → MARK(X)
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(nats) → ACTIVE(nats)
ACTIVE(tail(cons(X, L))) → MARK(L)

Used ordering: Polynomial interpretation [25,35]:

POL(tail(x₁)) = 1/4
POL(head(x₁)) = 1/4
POL(mark(x₁)) = 0
POL(0) = 4
POL(ACTIVE(x₁)) = (2)x_1
POL(cons(x₁, x₂)) = 0
POL(active(x₁)) = 11/4
POL(MARK(x₁)) = 1/2
POL(adx(x₁)) = 1/4
POL(incr(x₁)) = 1/4
POL(zeros) = 1/4
POL(s(x₁)) = 0
POL(nats) = 1/4
POL(nil) = 4

The value of delta used in the strict ordering is 1/2.
The following usable rules [17] were oriented:

s(active(X)) → s(X)
s(mark(X)) → s(X)
incr(active(X)) → incr(X)
incr(mark(X)) → incr(X)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
adx(active(X)) → adx(X)
adx(mark(X)) → adx(X)
head(active(X)) → head(X)
head(mark(X)) → head(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(nats) → MARK(adx(zeros))
MARK(adx(X)) → ACTIVE(adx(mark(X)))
ACTIVE(incr(cons(X, L))) → MARK(cons(s(X), incr(L)))
MARK(s(X)) → MARK(X)
MARK(tail(X)) → MARK(X)
MARK(head(X)) → MARK(X)
MARK(tail(X)) → ACTIVE(tail(mark(X)))
MARK(head(X)) → ACTIVE(head(mark(X)))
MARK(incr(X)) → ACTIVE(incr(mark(X)))
MARK(incr(X)) → MARK(X)
MARK(cons(X1, X2)) → MARK(X1)
ACTIVE(adx(cons(X, L))) → MARK(incr(cons(X, adx(L))))
MARK(adx(X)) → MARK(X)
ACTIVE(head(cons(X, L))) → MARK(X)
MARK(zeros) → ACTIVE(zeros)
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(nats) → ACTIVE(nats)
ACTIVE(tail(cons(X, L))) → MARK(L)

The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(tail(X)) → MARK(X)
MARK(head(X)) → MARK(X)
ACTIVE(head(cons(X, L))) → MARK(X)
ACTIVE(tail(cons(X, L))) → MARK(L)

The remaining pairs can at least be oriented weakly.

ACTIVE(nats) → MARK(adx(zeros))
MARK(adx(X)) → ACTIVE(adx(mark(X)))
ACTIVE(incr(cons(X, L))) → MARK(cons(s(X), incr(L)))
MARK(s(X)) → MARK(X)
MARK(tail(X)) → ACTIVE(tail(mark(X)))
MARK(head(X)) → ACTIVE(head(mark(X)))
MARK(incr(X)) → ACTIVE(incr(mark(X)))
MARK(incr(X)) → MARK(X)
MARK(cons(X1, X2)) → MARK(X1)
ACTIVE(adx(cons(X, L))) → MARK(incr(cons(X, adx(L))))
MARK(adx(X)) → MARK(X)
MARK(zeros) → ACTIVE(zeros)
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(nats) → ACTIVE(nats)

Used ordering: Polynomial interpretation [25,35]:

POL(tail(x₁)) = 1/4 + (4)x_1
POL(head(x₁)) = 1/4 + (2)x_1
POL(mark(x₁)) = x_1
POL(0) = 0
POL(ACTIVE(x₁)) = (1/2)x_1
POL(cons(x₁, x₂)) = (2)x_1 + (1/4)x_2
POL(active(x₁)) = x_1
POL(MARK(x₁)) = (1/2)x_1
POL(adx(x₁)) = x_1
POL(incr(x₁)) = x_1
POL(zeros) = 0
POL(s(x₁)) = x_1
POL(nats) = 0
POL(nil) = 0

The value of delta used in the strict ordering is 1/8.
The following usable rules [17] were oriented:

mark(0) → active(0)
s(active(X)) → s(X)
s(mark(X)) → s(X)
incr(active(X)) → incr(X)
incr(mark(X)) → incr(X)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
active(adx(nil)) → mark(nil)
adx(active(X)) → adx(X)
adx(mark(X)) → adx(X)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(adx(X)) → active(adx(mark(X)))
active(tail(cons(X, L))) → mark(L)
active(zeros) → mark(cons(0, zeros))
active(nats) → mark(adx(zeros))
mark(head(X)) → active(head(mark(X)))
mark(incr(X)) → active(incr(mark(X)))
mark(s(X)) → active(s(mark(X)))
mark(nats) → active(nats)
active(head(cons(X, L))) → mark(X)
mark(tail(X)) → active(tail(mark(X)))
active(incr(nil)) → mark(nil)
head(active(X)) → head(X)
head(mark(X)) → head(X)
mark(nil) → active(nil)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(nats) → MARK(adx(zeros))
MARK(adx(X)) → ACTIVE(adx(mark(X)))
ACTIVE(incr(cons(X, L))) → MARK(cons(s(X), incr(L)))
MARK(s(X)) → MARK(X)
MARK(tail(X)) → ACTIVE(tail(mark(X)))
MARK(head(X)) → ACTIVE(head(mark(X)))
MARK(incr(X)) → ACTIVE(incr(mark(X)))
MARK(incr(X)) → MARK(X)
MARK(cons(X1, X2)) → MARK(X1)
ACTIVE(adx(cons(X, L))) → MARK(incr(cons(X, adx(L))))
MARK(adx(X)) → MARK(X)
MARK(zeros) → ACTIVE(zeros)
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(nats) → ACTIVE(nats)

The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(tail(X)) → ACTIVE(tail(mark(X)))
MARK(head(X)) → ACTIVE(head(mark(X)))

The remaining pairs can at least be oriented weakly.

ACTIVE(nats) → MARK(adx(zeros))
MARK(adx(X)) → ACTIVE(adx(mark(X)))
ACTIVE(incr(cons(X, L))) → MARK(cons(s(X), incr(L)))
MARK(s(X)) → MARK(X)
MARK(incr(X)) → ACTIVE(incr(mark(X)))
MARK(incr(X)) → MARK(X)
MARK(cons(X1, X2)) → MARK(X1)
ACTIVE(adx(cons(X, L))) → MARK(incr(cons(X, adx(L))))
MARK(adx(X)) → MARK(X)
MARK(zeros) → ACTIVE(zeros)
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(nats) → ACTIVE(nats)

Used ordering: Polynomial interpretation [25,35]:

POL(tail(x₁)) = 0
POL(head(x₁)) = 0
POL(mark(x₁)) = 0
POL(0) = 3
POL(ACTIVE(x₁)) = x_1
POL(cons(x₁, x₂)) = 0
POL(active(x₁)) = 4
POL(MARK(x₁)) = 2
POL(adx(x₁)) = 2
POL(incr(x₁)) = 2
POL(zeros) = 2
POL(s(x₁)) = 4
POL(nats) = 2
POL(nil) = 13/4

The value of delta used in the strict ordering is 2.
The following usable rules [17] were oriented:

incr(active(X)) → incr(X)
incr(mark(X)) → incr(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
adx(active(X)) → adx(X)
adx(mark(X)) → adx(X)
head(active(X)) → head(X)
head(mark(X)) → head(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(nats) → MARK(adx(zeros))
MARK(adx(X)) → ACTIVE(adx(mark(X)))
MARK(adx(X)) → MARK(X)
ACTIVE(incr(cons(X, L))) → MARK(cons(s(X), incr(L)))
MARK(zeros) → ACTIVE(zeros)
MARK(s(X)) → MARK(X)
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(incr(X)) → MARK(X)
MARK(incr(X)) → ACTIVE(incr(mark(X)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(nats) → ACTIVE(nats)
ACTIVE(adx(cons(X, L))) → MARK(incr(cons(X, adx(L))))

The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(adx(X)) → MARK(X)
ACTIVE(incr(cons(X, L))) → MARK(cons(s(X), incr(L)))
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(incr(X)) → MARK(X)
ACTIVE(adx(cons(X, L))) → MARK(incr(cons(X, adx(L))))

The remaining pairs can at least be oriented weakly.

ACTIVE(nats) → MARK(adx(zeros))
MARK(adx(X)) → ACTIVE(adx(mark(X)))
MARK(zeros) → ACTIVE(zeros)
MARK(s(X)) → MARK(X)
MARK(incr(X)) → ACTIVE(incr(mark(X)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(nats) → ACTIVE(nats)

Used ordering: Polynomial interpretation [25,35]:

POL(tail(x₁)) = 7/4 + (4)x_1
POL(head(x₁)) = 1 + x_1
POL(mark(x₁)) = x_1
POL(0) = 0
POL(ACTIVE(x₁)) = (1/4)x_1
POL(cons(x₁, x₂)) = (4)x_1 + (1/4)x_2
POL(active(x₁)) = x_1
POL(MARK(x₁)) = (1/4)x_1
POL(adx(x₁)) = 5/4 + x_1
POL(incr(x₁)) = 1/4 + x_1
POL(zeros) = 3/4
POL(s(x₁)) = x_1
POL(nats) = 2
POL(nil) = 0

The value of delta used in the strict ordering is 3/64.
The following usable rules [17] were oriented:

mark(0) → active(0)
s(active(X)) → s(X)
s(mark(X)) → s(X)
incr(active(X)) → incr(X)
incr(mark(X)) → incr(X)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
active(adx(nil)) → mark(nil)
adx(active(X)) → adx(X)
adx(mark(X)) → adx(X)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(adx(X)) → active(adx(mark(X)))
active(tail(cons(X, L))) → mark(L)
active(zeros) → mark(cons(0, zeros))
active(nats) → mark(adx(zeros))
mark(head(X)) → active(head(mark(X)))
mark(incr(X)) → active(incr(mark(X)))
mark(s(X)) → active(s(mark(X)))
mark(nats) → active(nats)
active(head(cons(X, L))) → mark(X)
mark(tail(X)) → active(tail(mark(X)))
active(incr(nil)) → mark(nil)
head(active(X)) → head(X)
head(mark(X)) → head(X)
mark(nil) → active(nil)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(nats) → MARK(adx(zeros))
MARK(adx(X)) → ACTIVE(adx(mark(X)))
MARK(s(X)) → MARK(X)
MARK(zeros) → ACTIVE(zeros)
MARK(incr(X)) → ACTIVE(incr(mark(X)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(nats) → ACTIVE(nats)

The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 5 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

MARK(s(X)) → MARK(X)
MARK(cons(X1, X2)) → MARK(X1)

The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(s(X)) → MARK(X)
MARK(cons(X1, X2)) → MARK(X1)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(cons(x₁, x₂)) = 1/2 + (3/2)x_1
POL(MARK(x₁)) = (1/2)x_1
POL(s(x₁)) = 9/4 + x_1

The value of delta used in the strict ordering is 1/4.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

active(incr(nil)) → mark(nil)
active(incr(cons(X, L))) → mark(cons(s(X), incr(L)))
active(adx(nil)) → mark(nil)
active(adx(cons(X, L))) → mark(incr(cons(X, adx(L))))
active(nats) → mark(adx(zeros))
active(zeros) → mark(cons(0, zeros))
active(head(cons(X, L))) → mark(X)
active(tail(cons(X, L))) → mark(L)
mark(incr(X)) → active(incr(mark(X)))
mark(nil) → active(nil)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(adx(X)) → active(adx(mark(X)))
mark(nats) → active(nats)
mark(zeros) → active(zeros)
mark(0) → active(0)
mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
adx(mark(X)) → adx(X)
adx(active(X)) → adx(X)
head(mark(X)) → head(X)
head(active(X)) → head(X)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.